n:, f:({0..n}). (x:{0..n}. 0  f(x))  (0  sum(f(x) | x < n)) 

latex

Definitions	i  j , False, A, A  B, P & Q, i  j < k, suptype(S; T), S  T, , ff, tt, (i = j), if b then t else f fi , Y, t  T, primrec(n;b;c), sum(f(x) | x < k), x(s), P  Q, {i..j}, x:A. B(x), , P  Q, Unit, ,
Lemmas	ge wf, nat properties, primrec wf, not functionality wrt iff, assert of bnot, eqff to assert, not wf, bnot wf, assert of eq int, eqtt to assert, assert wf, iff transitivity, bool wf, eq int wf, int seg wf, le wf, nat wf